Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar14/LJB01SLASHjones4.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

p₃(m, n, s₁(r)) -> p₃(m, r, n)
p₃(m, s₁(n), 0) -> p₃(0, n, m)
p₃(m, 0, 0) -> m

Q is empty.

↳ QTRS

  ↳ Non-Overlap Check

Q restricted rewrite system:
The TRS R consists of the following rules:

p₃(m, n, s₁(r)) -> p₃(m, r, n)
p₃(m, s₁(n), 0) -> p₃(0, n, m)
p₃(m, 0, 0) -> m

Q is empty.

The TRS is non-overlapping. Hence, we can switch to innermost.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

p₃(m, n, s₁(r)) -> p₃(m, r, n)
p₃(m, s₁(n), 0) -> p₃(0, n, m)
p₃(m, 0, 0) -> m

The set Q consists of the following terms:

p₃(x0, x1, s₁(x2))
p₃(x0, s₁(x1), 0)
p₃(x0, 0, 0)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

P₃(m, n, s₁(r)) -> P₃(m, r, n)
P₃(m, s₁(n), 0) -> P₃(0, n, m)

The TRS R consists of the following rules:

p₃(m, n, s₁(r)) -> p₃(m, r, n)
p₃(m, s₁(n), 0) -> p₃(0, n, m)
p₃(m, 0, 0) -> m

The set Q consists of the following terms:

p₃(x0, x1, s₁(x2))
p₃(x0, s₁(x1), 0)
p₃(x0, 0, 0)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P₃(m, n, s₁(r)) -> P₃(m, r, n)
P₃(m, s₁(n), 0) -> P₃(0, n, m)

The TRS R consists of the following rules:

p₃(m, n, s₁(r)) -> p₃(m, r, n)
p₃(m, s₁(n), 0) -> p₃(0, n, m)
p₃(m, 0, 0) -> m

The set Q consists of the following terms:

p₃(x0, x1, s₁(x2))
p₃(x0, s₁(x1), 0)
p₃(x0, 0, 0)

We have to consider all minimal (P,Q,R)-chains.